Encode unknown generic type parameters with (declare-forall-sort) - #93

conditions

constrained with trait bounds

…<T>` for `T` in the body)

extern_spec_fn

Each fail file is its pass twin with one narrow break, checked to yield
`verification error: Unsat` with the pinned pcsat configuration:

- simple_loop, simple_loop_2int, loop_unbound: drop the `T::p(x)` precondition,
  so the first `a.f(v)` call has an unimplied precondition.
- simple_loop_call: the concrete `impl A for B` returns `x - 1`, violating the
  inherited `ensures p(result)` with `p(x) = x > 0`.
- generic_impl: drop `requires T::valid(x, v)`; the impl predicate is `"true"`,
  so this is the only observable break.
- option_map: return `None` in the `Some` arm.
- annot_simple_loop_self: `v = a.f(v) + 1` in the loop body, refuted through the
  explicit invariant.

No fail twin for simple_loop_self: with the trait predicate taking a `Self`
argument (`q_p<a0>`), pcsat times out (60s and 180s) on every break tried,
including the `requires(true)` weakening that is refuted in 0.3s for
simple_loop. Body-level breaks on the loop tests (`v = a.f(v) + 1`, `let mut
v = 0`, returning `0`) also time out unless the loop invariant is explicit;
the refutation needs a non-trivial instance of the forall predicate or a loop
unrolling that the solver does not find.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>

Small, feature-isolated tests (prefix `probe_`) that exercise one pattern each
from the Map/Take/Fuse/identity adapter impls, with a trivial trait instead of
the Iterator spec, so a failure is attributable to the feature. Each file's
header comment states the pattern; FIXME headers state the observed failure.

Verified (pass and fail twins):
- delegation to a generic field through `&self` and `&mut self`
  (probe_wrap_delegate_shared, probe_wrap_delegate_mut)
- `Option<Self::Item>` through a generic wrapper, rebuilt arm by arm and via a
  catch-all arm (probe_wrap_option_assoc, probe_wrap_option_assoc_catchall)
- an unused `F: FnMut` field (probe_generic_impl_two_params)
- a usize counter behind `&mut self` (probe_usize_counter); without
  `-C debug-assertions=off` this hits `unimplemented!` for SubWithOverflow
- `Some(ref mut it)` on an Option field (probe_option_field_reborrow_refmut)
- calling an `Fn` closure stored in a field (probe_field_closure_call_fn); the
  field has to be modelled as `model::Closure<F>` and the impl-level `F: Fn`
  bound repeated on the method, because build_closure_type_for_param only
  reads the companion function's own predicates.

Not verified (FIXME):
- probe_field_closure_call: the FnMut version is Unsat. FnMut pre!/post! specs
  are Unsat on this branch in general (closure_postcondition_fnmut.rs,
  closure_receiver_mut_model.rs fail the same way); FnOnce and Fn verify.
- probe_option_field_reborrow, probe_option_field_reborrow_int:
  `match &mut self.iter` on an Option field times out (also at 300s), even in
  a trait-free integer version; the extra Mut layer for the temporary
  reference is the only difference from the `ref mut` form that verifies.
- probe_option_field_reborrow_assign: the same reborrow followed by
  `self.iter = None` verifies in about 50s on some runs and times out on
  others.

Since delegation, associated-type Option returns, and the counter all verify,
the Unsat of the identity adapter (id.rs on iterator-adapters) points at the
Iterator::next specification rather than at a language feature.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>

With the rebuilt coar:latest image, probe_option_field_reborrow,
probe_option_field_reborrow_int and probe_option_field_reborrow_assign verify in
about a second each, so the timeout on `match &mut self.iter` was a solver
issue rather than a Thrust one. Drop their FIXME headers and add the two missing
fail twins: the integer probe adds 2 instead of 1, the trait probe negates the
inner predicate in the impl's `p` (swapping `it.f()` for the no-postcondition
`it.g()` still times out).

The rebuilt image also changes other results: it rejects .smt2 files that use a
sort before declaring it (`[sort_of_sexp] undeclared sort "Mut<a1>"` on
probe_generic_impl_two_params, generic_impl and map_no_closure), and answers
`unknown` instead of `unsat` for the fail twins of probe_wrap_delegate_shared
and probe_field_closure_call_fn.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>

`build_closure_type_for_param` read `predicates_of(fn).predicates`, which holds
only the predicates written on the function itself. A closure-typed parameter
whose `Fn*` bound sits on the enclosing `impl<F: FnMut(..)>` (the shape of an
iterator adapter storing its mapper) therefore had no function type, and a
`pre!`/`post!` on it panicked in `annot_fn` ("precondition used on a
non-closure parameter") unless the bound was repeated on the method.

Go through `GenericPredicates::instantiate` / `instantiate_identity`, which
walk the parent chain, so bounds from the impl or trait header are seen too.

probe_field_closure_call_fn.rs drops the redundant method-level bound and
still verifies (its fail twin is unchanged); probe_field_closure_call.rs drops
it as well and no longer panics (it stays Unsat, see its FIXME). No other
closure, fn_poly or traits test changes outcome.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>

…atures

`collect_sorts` gathered the sorts to emit as `declare-datatypes` from the
predicate-variable signatures and the clauses only. A sort that appears solely
in the parameter list of a forall predicate (`declare-forall-fun`) or in the
signature of a `#[thrust_macros::predicate]` (`define-fun`) was therefore
neither declared nor run through the Hoice renamer, and showed up raw in the
output, e.g. `(define-fun p_valid_... ((self_ Tuple<a0>) (x a1)) Bool true)`
or `(declare-forall-fun q_post_f_...<a1> (Mut<a1> Int Int) Bool)`. This
happens when the predicate is declared for a generic impl but never applied
in a clause, as in generic_impl.rs.

Older PCSat builds silently accepted these files; the rebuilt one rejects them
with `[sort_of_sexp] undeclared sort "Tuple<a0>"`. Collect the parameter and
type-parameter sorts of every registered `ForallPred` and the signature sorts
of every `UserDefinedPredDef` as well, so they are monomorphised, renamed and
declared before their first use like every other sort.

generic_impl.rs, probe_generic_impl_two_params.rs (pass and fail twins) and
fail/loop_invariant_fn_param_closure.rs verify again; the pass twin of the
latter now reaches the solver and gets Unsat instead of the parse error. Two
unit tests pin the declaration for a forall-pred-only and a
user-defined-pred-only sort.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>

A specification of a function without generics that calls a trait
predicate on a concrete type, e.g. `X::p(result)` where `X: A` is a
concrete impl, was emitted as a universally quantified forall predicate
`q_p_...<Tuple<Int>>` instead of the impl's `define-fun p_p_...` body.
Nothing constrains that forall-fun, so the goal clause could never be
proved and the file was Unsat regardless of the program.

The cause was `instantiate_generics` returning `None` whenever the owner
has no generic args: `to_formula_or_term` took that to mean "unresolved"
and routed the call to `refine::trait_forall_pred` even though
`Instance::try_resolve` had already resolved it to the impl item. In a
generic owner the identity args are non-empty, so the same code path
resolved correctly, which is why the existing traits tests did not catch
it.

An empty owner instantiation only means there is nothing to substitute,
so treat it as the identity and let `Instance::try_resolve` decide the
routing in both cases: a call on a concrete type resolves to the impl's
predicate, and a call that still depends on the owner's type parameters
(an `ImplSource::Param`) returns `None` and keeps the forall predicate.

Add tests/ui/{pass,fail}/traits/concrete_pred_nongeneric.rs pinning this
down: a non-generic `target() -> X` with `ensures(X::p(result))` where
`p` is `x > 0`, returning `X(1)` (pass) and `X(0)` (fail).

The same routing also hit a free `#[thrust::predicate]` called from a
non-generic function, so tests/ui/pass/annot_preds.rs verifies again. No
other closure, fn_poly, trait or traits/ test changes outcome.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>

The example was Unsat on its own account, independently of the predicate
routing bug fixed in the previous commit: `Y(-1)` violated `repeat`'s
precondition `T::p(*x)` at `repeat(&mut y, 5)`. Call `y.g()` first, whose
`ensures(Self::p(!self))` establishes the precondition.

With both fixed, PCSat still times out inferring the invariant of the
loop in the generic `repeat`, so spell it out the way
simple_loop_self_mut.rs does: `T::p(*b)` plus the prophecy link
`!b == !x.at_entry()`, with `x` rebound to `b` so the invariant can name
both the current `&mut` and the entry value.

The fail twin tests/ui/fail/traits/simple_loop_call_multi.rs drops the
`y.g()` call again.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>

simple_loop_self_mut.rs put `requires(Self::p(*self, !self, x))` on `f`, a
precondition on the callee's own prophecy. Each `a.f(v)` in the loop reborrows
`a` with a fresh, universally quantified final value, so no invariant can
establish that for an abstract `p` (the commit adding the file, 52ad0ae, already
marked it as not supported). Use the `&mut` analogue of simple_loop_self.rs
instead: `p(self, x)` with `requires(Self::p(*self, x))` and
`ensures(Self::p(!self, result))`. PCSat still needs the loop invariant spelled
out, so the loop carries `invariant!(|b: &mut T, ...| T::p(*b, v) && !b == !a.at_entry())`
with `a` rebound to `b`, because an `invariant!` cannot name both views of the
same `&mut` argument.

Its fail twin uses `v = b.f(v) + 1`. The simple_loop_self twin weakens the
precondition to `true`; the rebuilt PCSat refutes it in 0.3s where the previous
build timed out.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>

The tests keep their header comment describing which adapter pattern each
one isolates; the prefix added nothing.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>

A generic function's spec calling `<Bar<T> as Foo>::valid(..)`, the
predicate of a generic impl on a type that still contains the owner's type
parameter, resolves through `Instance::try_resolve` to the impl item and
uses its `define-fun` body; only a call on the type parameter itself
(`T::valid`) falls back to a forall predicate. This is the intended
behaviour of the routing changed in 4b4f0ac; the pair records it (both the
qualified-path and the `Bar::<T>::valid` spelling resolve the same way).

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>

The impl predicate bodies of these tests are SMT strings that refer to the
inner type's trait predicates by their hash-suffixed names (`q_p_<hash><a0>`).
The hash comes from the def path, which includes the crate name and hence the
file name, so 323a3b8 left every reference stale and PCSat failed with
`q_p_<old hash><a0> is not bound`. Regenerated with
.experimental/extract-predicate-hashes.py for the eight affected pairs.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>

The file, type and function names say what each test isolates; drop the
"Probe:" headers and the inline explanations, keep the one-line Rust
renderings of the SMT predicate bodies, and shorten the one remaining FIXME.
Remove option_field_reborrow_refmut: it only worked around a solver timeout
that the current PCSat build no longer has and matches no adapter pattern.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>

They were written to report macro and annotation typing problems, not to
guard behaviour, and the problems they describe are settled.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

Each pass file verifies against the `Iterator` specification it declares, and
its fail twin breaks only the property under test.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

`Ghost<T>` was known to the analyzer only through `impl<T: Model> Model for Ghost<T>`,
so `resolve_model_ty` had to normalize `<Ghost<T> as Model>::Ty` to learn anything about
it. In a function generic over `T` that normalization fails -- without a `T: Model` bound
rustc cannot select the impl -- and the fallback hands back the unmodeled Rust type, a
`PhantomData` newtype, which lowers to the singleton sort `(own (),)`. A parameter of
singleton sort is not bound in `relate_sub_param_types`, while the refinement lifted from
`#[requires(g == v)]` still names it, so building the entry obligation panicked with
`unbound var $0`.

Mark the struct and lower it structurally, the way `Closure<T>` already is: in the logic a
`Ghost<T>` is its content, so `model_adt` returns the content type directly and no trait
selection is involved. The `Model` impl stays, since a specification parameter still
lowers to `<Ghost<T> as Model>::Ty` and has to name it; a TODO on both sides records that
the two have to agree.

The `fail` twin still reports nothing: a generic function's parameter predicates never
occur in a clause head, so its body is discharged vacuously and its callers constrain a
separate pair -- the same gap the `fn_poly*` tests sit in.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

two_loops.rs and multi_params.rs time out while the loop invariants are being
inferred; these variants supply them by hand, as annot_simple_loop_self.rs does
for simple_loop_self.rs.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

The inference versions time out; these supply the inner loop's invariant by
hand, as annot_simple_loop_self.rs does for simple_loop_self.rs.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

… args

Generic function calls at concrete type arguments built a fresh function
type whose predicate variables were never constrained: the body was
analyzed once, with placeholder args, constraining a different set of
predicate variables. Call sites therefore learned nothing about the
callee, so assertions on returned values were left unchecked (unsound).

Re-analyze the monomorphized body at each concrete instantiation
(DefTy::Generic now uses DeferredDefMode::Analyze) so the fresh contract
predicate variables are constrained by the body. Basic-block types are
registered per analysis instance (AnalysisKey), so nested analyses of the
same def (e.g. recursive generics) no longer clobber each other, and
calls still carrying type parameters keep using the placeholder contract.

This fixes the known-bug in adt_generic_enum_helper_return and makes 18
previously silently-accepted fail tests report Unsat.

`InstantiationKey` carries `caller_def_id`, so a generic body is re-analyzed once per
(type arguments, calling function) rather than once per monomorphization. Record why it
cannot simply be dropped -- the caller's `owner_fn_id` is what interprets a `ParamTy`'s
index, so removing it would silently conflate type parameters declared in different
items -- and what would have to change for this to become a monomorphization cache.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

Two shapes that no test covered, both of which a change to how a def is routed
between the concrete and the generic analysis would silently alter.

A generic function whose signature does not mention its type parameter is analyzed
with a concrete contract, so a caller that is itself generic still learns its result.
Routing such a def to the generic analysis instead would leave the contract to a
re-analysis that a call at type arguments which are still type parameters never
triggers, and the caller would accept anything from that call onwards.

An annotated generic function contributes its contract at such a call site, where an
inferred one does not. The existing fn_poly_annot tests all call from `main` at
concrete arguments, which is the case that does not distinguish the two.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

`collect_forall_defaults` decided which `default_<sort>` constants to declare by
scanning the stored clause AST for `Term::ForallDefault`, and treated
`Term::ArrayEmpty` as a leaf. But the SMT-LIB2 writer synthesises
`Term::default_for(elem)` for an empty array at print time, so an array over an
abstract element sort emitted `default_a0` with no declaration and CoAR rejected
the file with `default_a0 is not bound`. Ask `default_for` itself which defaults
the writer will reference, so the two cannot drift.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

… impl

Lifting a formula out of an impl method replaced the type `Self` with the impl's
self type, turning the projection `Self::Item` into `<Wrap<I>>::Item`. `Self` in a
trait impl says which trait to look in; a bare ADT does not, so rustc rejected the
lifted `#[thrust::formula_fn]` with `E0223 ambiguous associated type` — and the
type annotations of nearby ghost terms failed to infer as a consequence. Carry the
implemented trait along and emit `<Wrap<I> as Iterator>::Item`. The trait-method
branch is unaffected: it substitutes a type parameter, whose bounds resolve the
projection on their own.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

Registering the contract of an `Fn`-bounded type parameter read the parameter's
index in the generics of the function being analysed. A bound declared on an impl
block was taken straight from `predicates_of(impl)`, which no instantiation has
touched, so an external call into that impl looked the impl's own parameter up in
the caller's table and hit `unknown type param idx`.

Resolve such a parameter through the arguments the analysis runs with before using
it, for both the sort it builds and the key it registers under. A parameter that
resolves to another generic caller's parameter is now recorded against that one;
a parameter that resolves to a concrete callable needs no parameter-keyed contract
at all, since the callable carries its own.

`build_closure_type_for_param` tried to do this by instantiating the `ParamTy`
itself, which is an identity by construction -- instantiating a `ParamTy` can only
yield a `ParamTy`, never the concrete argument. Bind the type instead.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

An `FnMut` closure receives its upvars behind a `&mut`, and its precondition took that whole
`Mut` pair. The pair's prophecy is still unconstrained where the precondition has to be
discharged -- the borrow resolves it only after the call -- so `pre!(f(..))`, which names the
upvars as they are, could never reach the obligation the call raises, and every `FnMut`
precondition needed a `forall` over the prophecy before it said anything at all.

Take the current value of the upvars in the precondition instead. A precondition is a property
of the state the call starts from, and the two states stay related by the postcondition, which
is unchanged. `closure_trait_call` now reports the `Fn` trait it resolved, so the projection
keys off that rather than off the shape of the receiver type.

Specs that spelled the receiver out as `Mut::new(f, g)` still mean what they meant, since the
projection drops `g`. The two-call tests gain the precondition they were missing: their upvars
have to satisfy it in every state the calls start from, which needs one binder now instead of
two. Their `fail` twins keep their old specification -- with the quantified precondition the
solver does not answer the negative direction within 180s.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

Twelve pass/fail pairs whose specifications verify in both directions on this
branch: a ghost `Seq` grown by a loop (`ghost_seq_loop`, and its `forall`
variant), the same history carried through a trait loop (`traits/ghost_produced`,
`traits/ghost_step_chain`, `traits/ghost_count`), fold specified with an `Fn`
and that history (`traits/fold_fn_ghost`, `_noiter`, `_call`, and `_call_law`,
the last discharging a call site by assuming an induction principle), and Map
with the closure's precondition stated three ways (`traits/map_fn_uncond_pre`
unconditionally, `traits/map_fn_concrete_item` at a concrete item type, and
`traits/map_ext_total_pre` over the produced history with a preservation law).

Each was run here after copying, all 24 files green. The remaining exploration
on iterator-adapters is not adopted: `traits/map` and `traits/map_fn` are the
superseded non-inductive Map invariant and still Unsat, and `traits/fold`,
`traits/fold_fn`, `traits/fuse`, `traits/map_no_closure` and `traits/skip` have
no fail twin to pin the other direction.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

The twin used to drop the empty-history precondition, which is the base
case of the loop invariant: it goes Unsat even when nothing carries
`item_ok` across an iteration, so it never pinned the property the pass
file is named for. Removing `next`'s `item_ok` postcondition instead
takes away the fact's only source.

Weakening the loop invariant or shifting the postcondition's index both
leave the solver at Unknown -- refuting those needs it to reason about
every interpretation of an abstract predicate.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

`trait_assoc_type_spec` asked Thrust to prove `nonempty`'s postcondition from an
empty default body. A default method is checked once against the abstract
predicate, so the claim has to hold for every implementor, and nothing in the
trait says `produces` is non-empty -- the `pass` file was claiming a capability
Thrust does not have (re-checking default bodies per impl) rather than pinning
one it does. Declaring `nonempty` without a body moves the obligation to the
impl, where `produces` is concrete, and the fail twin's `false` predicate still
refutes it.

`trait_default_method_spec` keeps the rejected shape as its own pair, so the
distinction between the two is pinned rather than lost.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>